es:ES, Qa, Rb:(EE), A, B:Type, Ia:AbsInterface(A), Ib:AbsInterface(B), f:(E(Ia)B),
g:(E(Ib)E).
g glues Ia:Qa f Ib:Rb   

latex

Definitions

False, {x:A| B(x)} , left + right, P  Q, Dec(P), x:A. B(x), b, let x,y = A in B(x;y), t.1, E, E(X), x:A  B(x), ES, x:AB(x), Type, AbsInterface(A), s = t, Q ==f== P, Q = f== P, f(a), f is Q-R-pre-preserving on P, Inj(A;B;f), {I}, t  T, Top, Void, x:A.B(x), P  Q, P & Q, <a, b>, EqDecider(T), Unit, IdLnk, Id, EOrderAxioms(E; pred?; info), EState(T), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, , constant_function(f;A;B), x. t(x), S  T, suptype(S; T), X(e), A c B, , x:A. B(x), g glues Ia:Qa f Ib:Rb, pred!(e;e'), SWellFounded(R(x;y)), loc(e), A

Lemmas

val-axiom wf, constant function wf, weak-antecedent-function wf, weak-antecedent-surjection wf, Q-R-pre-preserving wf, inject wf, es-interface-val wf, subtype rel weakening, ext-eq weakening, weak-antecedent-surjection-property, subtype rel set, subtype rel self, es-E-interface wf, subtype rel function, subtype rel sum, decidable assert